(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 2))
(let ((e4 (* (- e3) v0)))
(let ((e5 (+ e4 v1)))
(let ((e6 (+ v2 v1)))
(let ((e7 (> v0 e5)))
(let ((e8 (<= e5 e4)))
(let ((e9 (<= e6 e6)))
(let ((e10 (< e4 e6)))
(let ((e11 (< e5 e4)))
(let ((e12 (distinct e6 v2)))
(let ((e13 (= e5 v1)))
(let ((e14 (= e5 v0)))
(let ((e15 (>= e6 e5)))
(let ((e16 (> e4 e6)))
(let ((e17 (> v2 v2)))
(let ((e18 (distinct v0 v1)))
(let ((e19 (and e17 e7)))
(let ((e20 (not e15)))
(let ((e21 (ite e14 e10 e16)))
(let ((e22 (=> e11 e12)))
(let ((e23 (=> e18 e19)))
(let ((e24 (=> e8 e22)))
(let ((e25 (=> e20 e9)))
(let ((e26 (or e24 e13)))
(let ((e27 (ite e25 e23 e23)))
(let ((e28 (= e27 e27)))
(let ((e29 (or e26 e21)))
(let ((e30 (=> e28 e28)))
(let ((e31 (= e29 e30)))
e31
))))))))))))))))))))))))))))))

(check-sat)
